0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 10 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 1 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
sumB_in_gga([], [], []) → sumB_out_gga([], [], [])
sumB_in_gga(.(T10, T11), .(T12, T13), .(T16, T17)) → U3_gga(T10, T11, T12, T13, T16, T17, pA_in_ggagga(T10, T12, T16, T11, T13, T17))
pA_in_ggagga(0, T22, T22, T11, T13, T23) → U1_ggagga(T22, T11, T13, T23, sumB_in_gga(T11, T13, T23))
U1_ggagga(T22, T11, T13, T23, sumB_out_gga(T11, T13, T23)) → pA_out_ggagga(0, T22, T22, T11, T13, T23)
pA_in_ggagga(s(T30), T31, s(T33), T11, T13, T34) → U2_ggagga(T30, T31, T33, T11, T13, T34, pA_in_ggagga(T30, T31, T33, T11, T13, T34))
U2_ggagga(T30, T31, T33, T11, T13, T34, pA_out_ggagga(T30, T31, T33, T11, T13, T34)) → pA_out_ggagga(s(T30), T31, s(T33), T11, T13, T34)
U3_gga(T10, T11, T12, T13, T16, T17, pA_out_ggagga(T10, T12, T16, T11, T13, T17)) → sumB_out_gga(.(T10, T11), .(T12, T13), .(T16, T17))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
sumB_in_gga([], [], []) → sumB_out_gga([], [], [])
sumB_in_gga(.(T10, T11), .(T12, T13), .(T16, T17)) → U3_gga(T10, T11, T12, T13, T16, T17, pA_in_ggagga(T10, T12, T16, T11, T13, T17))
pA_in_ggagga(0, T22, T22, T11, T13, T23) → U1_ggagga(T22, T11, T13, T23, sumB_in_gga(T11, T13, T23))
U1_ggagga(T22, T11, T13, T23, sumB_out_gga(T11, T13, T23)) → pA_out_ggagga(0, T22, T22, T11, T13, T23)
pA_in_ggagga(s(T30), T31, s(T33), T11, T13, T34) → U2_ggagga(T30, T31, T33, T11, T13, T34, pA_in_ggagga(T30, T31, T33, T11, T13, T34))
U2_ggagga(T30, T31, T33, T11, T13, T34, pA_out_ggagga(T30, T31, T33, T11, T13, T34)) → pA_out_ggagga(s(T30), T31, s(T33), T11, T13, T34)
U3_gga(T10, T11, T12, T13, T16, T17, pA_out_ggagga(T10, T12, T16, T11, T13, T17)) → sumB_out_gga(.(T10, T11), .(T12, T13), .(T16, T17))
SUMB_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → U3_GGA(T10, T11, T12, T13, T16, T17, pA_in_ggagga(T10, T12, T16, T11, T13, T17))
SUMB_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → PA_IN_GGAGGA(T10, T12, T16, T11, T13, T17)
PA_IN_GGAGGA(0, T22, T22, T11, T13, T23) → U1_GGAGGA(T22, T11, T13, T23, sumB_in_gga(T11, T13, T23))
PA_IN_GGAGGA(0, T22, T22, T11, T13, T23) → SUMB_IN_GGA(T11, T13, T23)
PA_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → U2_GGAGGA(T30, T31, T33, T11, T13, T34, pA_in_ggagga(T30, T31, T33, T11, T13, T34))
PA_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → PA_IN_GGAGGA(T30, T31, T33, T11, T13, T34)
sumB_in_gga([], [], []) → sumB_out_gga([], [], [])
sumB_in_gga(.(T10, T11), .(T12, T13), .(T16, T17)) → U3_gga(T10, T11, T12, T13, T16, T17, pA_in_ggagga(T10, T12, T16, T11, T13, T17))
pA_in_ggagga(0, T22, T22, T11, T13, T23) → U1_ggagga(T22, T11, T13, T23, sumB_in_gga(T11, T13, T23))
U1_ggagga(T22, T11, T13, T23, sumB_out_gga(T11, T13, T23)) → pA_out_ggagga(0, T22, T22, T11, T13, T23)
pA_in_ggagga(s(T30), T31, s(T33), T11, T13, T34) → U2_ggagga(T30, T31, T33, T11, T13, T34, pA_in_ggagga(T30, T31, T33, T11, T13, T34))
U2_ggagga(T30, T31, T33, T11, T13, T34, pA_out_ggagga(T30, T31, T33, T11, T13, T34)) → pA_out_ggagga(s(T30), T31, s(T33), T11, T13, T34)
U3_gga(T10, T11, T12, T13, T16, T17, pA_out_ggagga(T10, T12, T16, T11, T13, T17)) → sumB_out_gga(.(T10, T11), .(T12, T13), .(T16, T17))
SUMB_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → U3_GGA(T10, T11, T12, T13, T16, T17, pA_in_ggagga(T10, T12, T16, T11, T13, T17))
SUMB_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → PA_IN_GGAGGA(T10, T12, T16, T11, T13, T17)
PA_IN_GGAGGA(0, T22, T22, T11, T13, T23) → U1_GGAGGA(T22, T11, T13, T23, sumB_in_gga(T11, T13, T23))
PA_IN_GGAGGA(0, T22, T22, T11, T13, T23) → SUMB_IN_GGA(T11, T13, T23)
PA_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → U2_GGAGGA(T30, T31, T33, T11, T13, T34, pA_in_ggagga(T30, T31, T33, T11, T13, T34))
PA_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → PA_IN_GGAGGA(T30, T31, T33, T11, T13, T34)
sumB_in_gga([], [], []) → sumB_out_gga([], [], [])
sumB_in_gga(.(T10, T11), .(T12, T13), .(T16, T17)) → U3_gga(T10, T11, T12, T13, T16, T17, pA_in_ggagga(T10, T12, T16, T11, T13, T17))
pA_in_ggagga(0, T22, T22, T11, T13, T23) → U1_ggagga(T22, T11, T13, T23, sumB_in_gga(T11, T13, T23))
U1_ggagga(T22, T11, T13, T23, sumB_out_gga(T11, T13, T23)) → pA_out_ggagga(0, T22, T22, T11, T13, T23)
pA_in_ggagga(s(T30), T31, s(T33), T11, T13, T34) → U2_ggagga(T30, T31, T33, T11, T13, T34, pA_in_ggagga(T30, T31, T33, T11, T13, T34))
U2_ggagga(T30, T31, T33, T11, T13, T34, pA_out_ggagga(T30, T31, T33, T11, T13, T34)) → pA_out_ggagga(s(T30), T31, s(T33), T11, T13, T34)
U3_gga(T10, T11, T12, T13, T16, T17, pA_out_ggagga(T10, T12, T16, T11, T13, T17)) → sumB_out_gga(.(T10, T11), .(T12, T13), .(T16, T17))
SUMB_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → PA_IN_GGAGGA(T10, T12, T16, T11, T13, T17)
PA_IN_GGAGGA(0, T22, T22, T11, T13, T23) → SUMB_IN_GGA(T11, T13, T23)
PA_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → PA_IN_GGAGGA(T30, T31, T33, T11, T13, T34)
sumB_in_gga([], [], []) → sumB_out_gga([], [], [])
sumB_in_gga(.(T10, T11), .(T12, T13), .(T16, T17)) → U3_gga(T10, T11, T12, T13, T16, T17, pA_in_ggagga(T10, T12, T16, T11, T13, T17))
pA_in_ggagga(0, T22, T22, T11, T13, T23) → U1_ggagga(T22, T11, T13, T23, sumB_in_gga(T11, T13, T23))
U1_ggagga(T22, T11, T13, T23, sumB_out_gga(T11, T13, T23)) → pA_out_ggagga(0, T22, T22, T11, T13, T23)
pA_in_ggagga(s(T30), T31, s(T33), T11, T13, T34) → U2_ggagga(T30, T31, T33, T11, T13, T34, pA_in_ggagga(T30, T31, T33, T11, T13, T34))
U2_ggagga(T30, T31, T33, T11, T13, T34, pA_out_ggagga(T30, T31, T33, T11, T13, T34)) → pA_out_ggagga(s(T30), T31, s(T33), T11, T13, T34)
U3_gga(T10, T11, T12, T13, T16, T17, pA_out_ggagga(T10, T12, T16, T11, T13, T17)) → sumB_out_gga(.(T10, T11), .(T12, T13), .(T16, T17))
SUMB_IN_GGA(.(T10, T11), .(T12, T13), .(T16, T17)) → PA_IN_GGAGGA(T10, T12, T16, T11, T13, T17)
PA_IN_GGAGGA(0, T22, T22, T11, T13, T23) → SUMB_IN_GGA(T11, T13, T23)
PA_IN_GGAGGA(s(T30), T31, s(T33), T11, T13, T34) → PA_IN_GGAGGA(T30, T31, T33, T11, T13, T34)
SUMB_IN_GGA(.(T10, T11), .(T12, T13)) → PA_IN_GGAGGA(T10, T12, T11, T13)
PA_IN_GGAGGA(0, T22, T11, T13) → SUMB_IN_GGA(T11, T13)
PA_IN_GGAGGA(s(T30), T31, T11, T13) → PA_IN_GGAGGA(T30, T31, T11, T13)
From the DPs we obtained the following set of size-change graphs: